1. Field of the Invention
This invention relates to a system for checking the equivalence of combinational circuits. More particularly, this invention relates to a system for checking such equivalence which is more robust than other systems heretofore achieved, and which accommodates the checking of complex circuits having substantial dissimilarities. The invention is embodied in a system, a method, and a program product for combinational equivalence checking.
2. Background and Related Art
A combinational circuit, as the term is used herein, is a circuit having a network of interconnected logic gates. Combinational circuits may be represented by logic netlists. A given combinational circuit has a fanin and a fanout. The fanin of a combinational circuit relates, in general, to the inputs provided to the combinational circuit. The fanout of a combinational. circuit relates to the set of outputs given by the combinational circuit. Thus, from a given point in a combinational circuit, the fanin side of the combinational circuit is the side closer to the inputs, and the fanout side is the side closer to the outputs. The relationship of the combinational circuit outputs to the combinational circuit inputs defines the overall functionality of the combinational circuit.
It is well known that, to design a combinational circuit with a predetermined overall functionality, many different combinational circuit structures are possible. In other words, two combinational circuits may structurally be very different in terms of the exact network of interconnected logic gates used, but may actually have an identical overall functionality.
Digital design involves the creation of combinational circuits. Frequently, digital design also involves the modification of an existing combinational circuit. Sometimes, it is desirable to modify an existing combinational circuit in only a structural manner, leaving the overall functionality of the changed combinational circuit the same as that of the existing combinational circuit.
Combinational circuits can be extremely complex, and the verification that one combinational circuit has the identical overall functionality of another combinational circuit is an important problem. This problem will be referred to as the combinational logic verification problem. This problem applies equally to the situation in which it is desired to verify that a node in one combinational circuit, as opposed to the combinational circuit as a whole, provides the same overall functionality as a node in another combinational circuit. Thus, it will be appreciated that the combinational logic verification problem relates to combinational circuits as a whole, and also to smaller combinational circuits within larger combinational circuits.
Below, the terms combinational circuits and nodes of combinational circuits will usually be interchangeably used. The two terms will usually be interchangeable because of the simple fact that a large logic netlist will always have nodes within it, and each of the nodes may define a smaller part of the overall combinational circuit which itself, taken alone, could be taken as a combinational circuit.
The combinational logic verification problem may be framed, conceptually, in terms of what is known in the art as a miter circuit. FIG. 1 illustrates a miter circuit 10. In FIG. 1, Circuit 1 and Circuit 2 are combinational circuits. It is desired to verify whether Circuit 1 and Circuit 2 are equivalent, i.e., whether the two combinational circuits have an identical overall functionality. In the example of FIG. 1, each of the two combinational circuits receives identical inputs w and x. Circuit 1 has, as a respective output, output y. Circuit 2 has, as a respective output, output y'. The nodes to be checked for equivalence provide their respective outputs y and y' to an XOR gate. The output of the XOR gate is output z. As useful background on the miter circuit, the following document is incorporated by reference:
D. Brand. Verification of large synthesized designs. In Proceedings of the IEEE International Conference on Computer-Aided Design, pages 534-537, November 1993. PA1 C. Berman and L. H. Trevyllian. Functional comparison of logic design for VLSI circuits. In Proceedings of the IEEE International Conference on Computer-Aided Design, pages 456-459. EKE Computer Society Press, Los Alamitos, Calif., November 1989. PA1 E. Cerny and C. Mauras. Tautology checking using cross-controllability and cross-observability relations. In Proceedings of the IEEE International Conference on Computer-Aided Design, pages 34-37. IEEE Computer Society Press, Los Alamitos, Calif., November 1990. PA1 J. Jain, R. Mukherjee, and M. Fujita. Advanced verification techniques based on learning. In Proceedings of the 32.sup.nd ACM/IEEE Design Automation Conference, pages 420-426. EKE Computer Society Press, Los Alamitos, Calif., June 1995. PA1 W. Kunz and D. Pradhan. Recursive learning: A new implication technique for efficient solutions to CAD problems--test, verification and optimization. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(9):1143-1158, September 1994. PA1 Y. Matsunaga. An efficient equivalence checker for combinational circuits. In Proceedings of the ACM/IEEE Design Automation Conference, pages 629-634. IEEE Computer Society Press, Los Alamitos, Calif., June 1996. PA1 D. Pradhan, D. Paul, and M. Chatterjee. Verilat: Verification using logic augmentation and transformations. In Proceedings of the IEEE International Conference on Computer-Aided Design, pages 88-95. IEEE Computer Society Press, Los Alamitos, Calif., November 1996. PA1 S. M. Reddy, W. Kunz, and D. Pradhan. Novel verification framework combining structural and OBDD methods in a synthesis environment. In Proceedings of the 32.sup.nd ACM/IEEE Design Automation Conference, pages 414-419. IEEE Computer Society Press, Los Alamitos, Calif., June 1995. PA1 J. P. Billon and J. C. Madre. Original concepts of PRIAM, an industrial tool for efficient formal verification of combinational circuits. In G. J. Milne, editor, Fusion of Hardware Design and Verification, pages 487-501. North-Holland, Amsterdam, 1988. PA1 M. Fujita, H. Fujisawa, and N. Kawato. Evaluation and improvements of a Boolean comparison program based on Binary Decision Diagrams. In Proceedings of the IEEE International Conference on Computer-Aided Design, pages 2-5. EKE Computer Society Press, Los Alamitos, Calif., 1988. PA1 S. Malik, R. K. Wang, A. Brayton, and A. Sangiovanni-Vincentelli. Logic verification using Binary Decision Diagrams in a logic synthesis environment. In Proceedings of the IEEE International Conference on Computer-Aided Design, pages 6-9. EKE Computer Society Press, Los Alamitos, Calif., 1988. PA1 R. E. Bryant. On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Transactions on Computers, 40(2):205213, February 1991.
As it will be appreciated, for every possible set of inputs w and x, if the combinational circuits are equivalent, outputs y and y' should always be identical. Whenever outputs y and y' are identical, the output z of the XOR gate will be 0. If, however, it is possible to obtain a 1 at output z, then the circuits are not perfectly equivalent.
The miter circuit 10 provides a unifying theme throughout the various approaches to solving the combinational logic verification problem.
One approach to solving the combinational logic verification problem is a structural approach. Under the structural approach, the miter circuit is used in an inner loop of an iterative equivalence checking framework. That is, nodes from Circuit 1 and Circuit 2 are compared. Nodes found to be equivalent are replaced, and the equivalence checking proceeds in a bottom up manner. As more nodes in each of the circuits are replaced, it becomes more possible to achieve a simplified check of the primary outputs. This structural approach, or iterative replacement approach, works well when Circuit 1 and Circuit 2 are structurally similar. The following documents are incorporated by reference for their useful background material on the structural approach:
Although combinational circuits sought to be compared may often be similar, there are many instances in which one circuit is much different from another. For example, when circuits are redesigned using automated design software, the redesigned circuit may have very little structural similarity to the original circuit. In such a case, the iterative replacement approach becomes very difficult because it is harder to pick out nodes in each of the two combinational circuits that actually are equivalent. The particular methods recommended in the above-identified background documents fail when there is little internal correspondence to exploit.
Another approach to the combinational logic verification problem is a functional approach. Under the functional approach use is made of binary decision diagrams (BDDs). A BDD results from reducing the entire combinational circuit to a canonical form. The following documents are incorporated by reference in their entirety as providing useful background information concerning function-based approaches:
Once each combinational circuit is reduced to a BDD, the problem of checking for equivalence is changed from the complex problem of comparing two different combinational circuits to the more simple problem of comparing two canonical data structures (i.e., BDDs).
The functional approach has shortcomings, however. Usually, a function-based approach uses some variant of the Reduced Ordered BDD (ROBDD). The ROBDD is discussed below, but additional background information on this topic may be found in the following document which is herein incorporated by reference: R. E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, C-35(8):677-691, August 1986. In particular, such BDDs grow exponentially in terms of the number of input variables for certain very commonly used logic functions like multipliers, as described in the following document now incorporated by reference for its background information in this regard:
Thus, such BDDs do not scale well, even for random logic. In other words, the larger the combinational circuit, the larger the BDDs, and the more difficult it becomes to use the functional approach. It is substantially impractical to use the functional approach to solve the combinational logic verification problem for very large combinational circuits.
Thus, the structural approach becomes impractical when the two combinational circuits are structurally dissimilar. The functional approach becomes impractical when the two combinational circuits are very large.